(set-logic QF_UF)
(declare-fun f (Bool) Bool)
(declare-fun g (Bool Bool) Bool)
(declare-fun P () Bool)
(declare-fun Q () Bool)
(push 1)
(assert (g (= P Q) Q))
(check-sat)
(assert (f P))
(pop 1)
(check-sat)
(exit)
